$\forall$${\it da}$:$k$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. normal{-}da\{i:l\}(${\it da}$) $\in$ Prop$_{\mbox{\scriptsize i'}}$